Module isotope::term[][src]

Expand description

Terms in isotope’s underlying dependent type system

Modules

dynamic

Dynamic terms, which allow run-time extension of isotope, mainly for testing and debugging purposes

flags

Flags for isotope terms

weak

Weak references to isotope terms

Structs

Annotation

An owned type annotation

App

A function application, with an optional type annotation

Case

A case expression, which switches on variants to return a value

Code

The hash-code of a value

Enum

A type with a finite number of named variants

Id

The identity type, representing proofs that two terms are equal

Lambda

A lambda function

Pi

A dependent function type

Refl

The reflexivity axiom: asserts that the left hand side and right hand side are judgementally equal, and therefore propositionally equal

TermId

A term in isotope’s term language

Universe

A typing universe

UniverseTerm

A term containing a typing universe

Var

A variable, represented by a de-Bruijn index

VarFilter

A filter for variables

Variant

A variant of an enumeration

Enums

AnnotationRef

A borrowed type annotation

Form

Forms a term can be in

Term

An enumeration of terms in isotope’s term language

Traits

AnnotationLike

A term which behaves like a (potentially borrowed) annotation

Cons

Objects which can be consed in a context

HasDependencies

Objects which have value dependencies

OptionalValue

A convenience trait implemented by Option<V> where V is a value

Substitute

Objects which can be substituted in a context

TermEq

Objects which may be determined equivalent by terms

Typecheck

Objects which can be type-checked in a context

Value

A trait implemented by values in isotope’s term language